The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
    ↳3 CpxTrsMatchBoundsTAProof (⇔, 109 ms)
    ↳4 BOUNDS(1, n^1)
    ↳5 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
        ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳8 CdtProblem
        ↳9 CdtUsableRulesProof (⇔, 0 ms)
        ↳10 CdtProblem
        ↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 181 ms)
        ↳12 CdtProblem
        ↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 43 ms)
        ↳14 CdtProblem
        ↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 16 ms)
        ↳16 CdtProblem
        ↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 64 ms)
        ↳18 CdtProblem
        ↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 58 ms)
        ↳20 CdtProblem
        ↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 78 ms)
        ↳22 CdtProblem
        ↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 1 ms)
        ↳24 CdtProblem
        ↳25 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳26 CdtProblem
        ↳27 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳28 CdtProblem
        ↳29 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳30 CdtProblem
        ↳31 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳32 CdtProblem
        ↳33 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳34 CdtProblem
        ↳35 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳36 CdtProblem
        ↳37 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳38 CdtProblem
        ↳39 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳40 CdtProblem
        ↳41 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳42 CdtProblem
        ↳43 CdtRewritingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳44 CdtProblem
        ↳45 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳46 CdtProblem
        ↳47 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳48 CdtProblem
        ↳49 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳50 CdtProblem
        ↳51 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳52 CdtProblem
        ↳53 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳54 CdtProblem
        ↳55 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
        ↳56 CdtProblem
        ↳57 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳58 CdtProblem
        ↳59 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳60 CdtProblem
        ↳61 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳62 CdtProblem
        ↳63 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳64 CdtProblem
        ↳65 CdtUnreachableProof (⇔, 0 ms)
        ↳66 CdtProblem
        ↳67 CdtUsableRulesProof (⇔, 0 ms)
        ↳68 CdtProblem
        ↳69 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 0 ms)
        ↳70 CdtProblem
        ↳71 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳72 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of top: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of active: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of f: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of start: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of match: active, start, proper, top, f, check, match
The following defined symbols can occur below the 0th argument of check: active, start, proper, top, f, check, match

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
match(f(x), f(y)) → f(match(x, y))
proper(f(x)) → f(proper(x))

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

proper(c) → ok(c)
f(mark(x)) → mark(f(x))
f(ok(x)) → ok(f(x))
active(f(x)) → f(active(x))
top(mark(x)) → top(check(x))
top(active(c)) → top(mark(c))
top(found(x)) → top(active(x))
check(f(x)) → f(check(x))
f(found(x)) → found(f(x))
active(f(x)) → mark(x)
start(ok(x)) → found(x)
match(X, x) → proper(x)
check(x) → start(match(f(X), x))

Rewrite Strategy: INNERMOST

(3) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 3.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6, 7]
transitions:
c0() → 0
ok0(0) → 0
mark0(0) → 0
found0(0) → 0
X0() → 0
proper0(0) → 1
f0(0) → 2
active0(0) → 3
top0(0) → 4
check0(0) → 5
start0(0) → 6
match0(0, 0) → 7
c1() → 8
ok1(8) → 1
f1(0) → 9
mark1(9) → 2
f1(0) → 10
ok1(10) → 2
check1(0) → 11
top1(11) → 4
active1(0) → 12
top1(12) → 4
f1(0) → 13
found1(13) → 2
found1(0) → 6
proper1(0) → 7
X1() → 16
f1(16) → 15
match1(15, 0) → 14
start1(14) → 5
ok1(8) → 7
mark1(9) → 9
mark1(9) → 10
mark1(9) → 13
ok1(10) → 9
ok1(10) → 10
ok1(10) → 13
c1() → 18
mark1(18) → 17
top1(17) → 4
found1(13) → 9
found1(13) → 10
found1(13) → 13
X2() → 21
f2(21) → 20
match2(20, 0) → 19
start2(19) → 11
check2(18) → 22
top2(22) → 4
X3() → 25
f3(25) → 24
match3(24, 18) → 23
start3(23) → 22

(4) BOUNDS(1, n^1)

(5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

proper(c) → ok(c)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
top(mark(z0)) → top(check(z0))
top(active(c)) → top(mark(c))
top(found(z0)) → top(active(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
start(ok(z0)) → found(z0)
match(X, z0) → proper(z0)
Tuples:

PROPER(c) → c1
F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
ACTIVE(f(z0)) → c6
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
CHECK(z0) → c11(START(match(f(X), z0)), MATCH(f(X), z0), F(X))
START(ok(z0)) → c12
MATCH(X, z0) → c13(PROPER(z0))
S tuples:

PROPER(c) → c1
F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
ACTIVE(f(z0)) → c6
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
CHECK(z0) → c11(START(match(f(X), z0)), MATCH(f(X), z0), F(X))
START(ok(z0)) → c12
MATCH(X, z0) → c13(PROPER(z0))
K tuples:none
Defined Rule Symbols:

proper, f, active, top, check, start, match

Defined Pair Symbols:

PROPER, F, ACTIVE, TOP, CHECK, START, MATCH

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing nodes:

MATCH(X, z0) → c13(PROPER(z0))
START(ok(z0)) → c12
ACTIVE(f(z0)) → c6
CHECK(z0) → c11(START(match(f(X), z0)), MATCH(f(X), z0), F(X))
PROPER(c) → c1

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

proper(c) → ok(c)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
top(mark(z0)) → top(check(z0))
top(active(c)) → top(mark(c))
top(found(z0)) → top(active(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
start(ok(z0)) → found(z0)
match(X, z0) → proper(z0)
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
K tuples:none
Defined Rule Symbols:

proper, f, active, top, check, start, match

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

proper(c) → ok(c)
top(mark(z0)) → top(check(z0))
top(active(c)) → top(mark(c))
top(found(z0)) → top(active(z0))
start(ok(z0)) → found(z0)
match(X, z0) → proper(z0)

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
K tuples:none
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(active(c)) → c8(TOP(mark(c)))
We considered the (Usable) Rules:

check(f(z0)) → f(check(z0))
active(f(z0)) → mark(z0)
f(found(z0)) → found(f(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(z0)) → f(active(z0))
check(z0) → start(match(f(X), z0))
And the Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(CHECK(x1)) = 0   
POL(F(x1)) = 0   
POL(TOP(x1)) = x1   
POL(X) = 0   
POL(active(x1)) = x1   
POL(c) = [1]   
POL(c10(x1, x2)) = x1 + x2   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c7(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(check(x1)) = 0   
POL(f(x1)) = 0   
POL(found(x1)) = x1   
POL(mark(x1)) = 0   
POL(match(x1, x2)) = 0   
POL(ok(x1)) = 0   
POL(start(x1)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
We considered the (Usable) Rules:

check(f(z0)) → f(check(z0))
active(f(z0)) → mark(z0)
f(found(z0)) → found(f(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(z0)) → f(active(z0))
check(z0) → start(match(f(X), z0))
And the Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(CHECK(x1)) = 0   
POL(F(x1)) = 0   
POL(TOP(x1)) = x1   
POL(X) = 0   
POL(active(x1)) = 0   
POL(c) = 0   
POL(c10(x1, x2)) = x1 + x2   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c7(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(check(x1)) = 0   
POL(f(x1)) = x1   
POL(found(x1)) = [1] + x1   
POL(mark(x1)) = 0   
POL(match(x1, x2)) = 0   
POL(ok(x1)) = 0   
POL(start(x1)) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
We considered the (Usable) Rules:

check(f(z0)) → f(check(z0))
active(f(z0)) → mark(z0)
f(found(z0)) → found(f(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(z0)) → f(active(z0))
check(z0) → start(match(f(X), z0))
And the Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(CHECK(x1)) = 0   
POL(F(x1)) = 0   
POL(TOP(x1)) = x1   
POL(X) = 0   
POL(active(x1)) = [1]   
POL(c) = 0   
POL(c10(x1, x2)) = x1 + x2   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c7(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(check(x1)) = 0   
POL(f(x1)) = x1   
POL(found(x1)) = [1]   
POL(mark(x1)) = [1]   
POL(match(x1, x2)) = 0   
POL(ok(x1)) = 0   
POL(start(x1)) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
We considered the (Usable) Rules:

check(f(z0)) → f(check(z0))
active(f(z0)) → mark(z0)
f(found(z0)) → found(f(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(z0)) → f(active(z0))
check(z0) → start(match(f(X), z0))
And the Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [2] + [2]x1   
POL(CHECK(x1)) = x1   
POL(F(x1)) = x1   
POL(TOP(x1)) = x1 + x12   
POL(X) = [1]   
POL(active(x1)) = x1   
POL(c) = [1]   
POL(c10(x1, x2)) = x1 + x2   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c7(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(check(x1)) = 0   
POL(f(x1)) = [2]x1   
POL(found(x1)) = [1] + x1   
POL(mark(x1)) = x1   
POL(match(x1, x2)) = [1]   
POL(ok(x1)) = [2] + x1   
POL(start(x1)) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
We considered the (Usable) Rules:

check(f(z0)) → f(check(z0))
active(f(z0)) → mark(z0)
f(found(z0)) → found(f(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(z0)) → f(active(z0))
check(z0) → start(match(f(X), z0))
And the Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [1] + x1   
POL(CHECK(x1)) = 0   
POL(F(x1)) = 0   
POL(TOP(x1)) = [2]x12   
POL(X) = [2]   
POL(active(x1)) = x1   
POL(c) = 0   
POL(c10(x1, x2)) = x1 + x2   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c7(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(check(x1)) = x1   
POL(f(x1)) = [1] + x1   
POL(found(x1)) = [1] + x1   
POL(mark(x1)) = x1   
POL(match(x1, x2)) = x2   
POL(ok(x1)) = [2] + x1   
POL(start(x1)) = x1   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
We considered the (Usable) Rules:

check(f(z0)) → f(check(z0))
active(f(z0)) → mark(z0)
f(found(z0)) → found(f(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(z0)) → f(active(z0))
check(z0) → start(match(f(X), z0))
And the Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(CHECK(x1)) = [2]x1   
POL(F(x1)) = 0   
POL(TOP(x1)) = [2]x12   
POL(X) = [1]   
POL(active(x1)) = [2] + x1   
POL(c) = 0   
POL(c10(x1, x2)) = x1 + x2   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c7(x1, x2)) = x1 + x2   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(check(x1)) = [1] + x1   
POL(f(x1)) = [1] + x1   
POL(found(x1)) = [2] + x1   
POL(mark(x1)) = [2] + x1   
POL(match(x1, x2)) = [1] + x2   
POL(ok(x1)) = x1   
POL(start(x1)) = x1   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, ACTIVE, TOP, CHECK

Compound Symbols:

c2, c3, c4, c5, c7, c8, c9, c10

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0)) by

ACTIVE(f(f(z0))) → c5(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
ACTIVE(f(f(z0))) → c5(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, CHECK, ACTIVE

Compound Symbols:

c2, c3, c4, c7, c8, c9, c10, c5

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0)) by

TOP(mark(f(z0))) → c7(TOP(f(check(z0))), CHECK(f(z0)))
TOP(mark(z0)) → c7(TOP(start(match(f(X), z0))), CHECK(z0))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
ACTIVE(f(f(z0))) → c5(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(f(z0))) → c7(TOP(f(check(z0))), CHECK(f(z0)))
TOP(mark(z0)) → c7(TOP(start(match(f(X), z0))), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, CHECK, ACTIVE

Compound Symbols:

c2, c3, c4, c8, c9, c10, c5, c7

(27) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
ACTIVE(f(f(z0))) → c5(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(f(z0))) → c7(TOP(f(check(z0))), CHECK(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, CHECK, ACTIVE

Compound Symbols:

c2, c3, c4, c8, c9, c10, c5, c7, c7

(29) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0)) by

CHECK(f(f(z0))) → c10(F(f(check(z0))), CHECK(f(z0)))
CHECK(f(z0)) → c10(F(start(match(f(X), z0))), CHECK(z0))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(f(z0))) → c7(TOP(f(check(z0))), CHECK(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(f(z0))) → c10(F(f(check(z0))), CHECK(f(z0)))
CHECK(f(z0)) → c10(F(start(match(f(X), z0))), CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c7, c10

(31) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(f(z0))) → c7(TOP(f(check(z0))), CHECK(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(f(z0))) → c10(F(f(check(z0))), CHECK(f(z0)))
CHECK(f(z0)) → c10(CHECK(z0))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c7, c10, c10

(33) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(f(f(z0))) → c5(F(f(active(z0))), ACTIVE(f(z0))) by

ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
ACTIVE(f(f(f(z0)))) → c5(F(f(mark(z0))), ACTIVE(f(f(z0))))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(f(z0))) → c7(TOP(f(check(z0))), CHECK(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(f(z0))) → c10(F(f(check(z0))), CHECK(f(z0)))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
ACTIVE(f(f(f(z0)))) → c5(F(f(mark(z0))), ACTIVE(f(f(z0))))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c7, c10, c10

(35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace TOP(mark(f(z0))) → c7(TOP(f(check(z0))), CHECK(f(z0))) by

TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(TOP(f(start(match(f(X), z0)))), CHECK(f(z0)))

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(f(z0))) → c10(F(f(check(z0))), CHECK(f(z0)))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
ACTIVE(f(f(f(z0)))) → c5(F(f(mark(z0))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(TOP(f(start(match(f(X), z0)))), CHECK(f(z0)))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c10, c10, c7

(37) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(f(z0))) → c10(F(f(check(z0))), CHECK(f(z0)))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
ACTIVE(f(f(f(z0)))) → c5(F(f(mark(z0))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c10, c10, c7

(39) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace CHECK(f(f(z0))) → c10(F(f(check(z0))), CHECK(f(z0))) by

CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(F(f(start(match(f(X), z0)))), CHECK(f(z0)))

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
ACTIVE(f(f(f(z0)))) → c5(F(f(mark(z0))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(F(f(start(match(f(X), z0)))), CHECK(f(z0)))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c10, c7, c10

(41) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
ACTIVE(f(f(f(z0)))) → c5(F(f(mark(z0))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c10, c7, c10

(43) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace ACTIVE(f(f(f(z0)))) → c5(F(f(mark(z0))), ACTIVE(f(f(z0)))) by ACTIVE(f(f(f(z0)))) → c5(F(mark(f(z0))), ACTIVE(f(f(z0))))

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(z0)) → c2(F(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
ACTIVE(f(f(f(z0)))) → c5(F(mark(f(z0))), ACTIVE(f(f(z0))))
S tuples:

F(mark(z0)) → c2(F(z0))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c2, c3, c4, c8, c9, c5, c7, c10, c7, c10

(45) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(mark(z0)) → c2(F(z0)) by

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
ACTIVE(f(f(f(z0)))) → c5(F(mark(f(z0))), ACTIVE(f(f(z0))))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c3, c4, c8, c9, c5, c7, c10, c7, c10, c2

(47) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(ok(z0)) → c3(F(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c3, c4, c8, c9, c5, c7, c10, c7, c10, c2, c5

(49) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(ok(z0)) → c3(F(z0)) by

F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(found(z0)) → c4(F(z0))
TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
F(found(z0)) → c4(F(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F, TOP, ACTIVE, CHECK

Compound Symbols:

c4, c8, c9, c5, c7, c10, c7, c10, c2, c5, c3

(51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(found(z0)) → c4(F(z0)) by

F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0)))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

TOP, ACTIVE, CHECK, F

Compound Symbols:

c8, c9, c5, c7, c10, c7, c10, c2, c5, c3, c4

(53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace ACTIVE(f(f(z0))) → c5(F(mark(z0)), ACTIVE(f(z0))) by

ACTIVE(f(f(f(y0)))) → c5(F(mark(f(y0))), ACTIVE(f(f(y0))))
ACTIVE(f(f(f(f(y0))))) → c5(F(mark(f(f(y0)))), ACTIVE(f(f(f(y0)))))
ACTIVE(f(f(mark(y0)))) → c5(F(mark(mark(y0))), ACTIVE(f(mark(y0))))
ACTIVE(f(f(ok(y0)))) → c5(F(mark(ok(y0))), ACTIVE(f(ok(y0))))
ACTIVE(f(f(found(y0)))) → c5(F(mark(found(y0))), ACTIVE(f(found(y0))))

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
ACTIVE(f(f(f(y0)))) → c5(F(mark(f(y0))), ACTIVE(f(f(y0))))
ACTIVE(f(f(f(f(y0))))) → c5(F(mark(f(f(y0)))), ACTIVE(f(f(f(y0)))))
ACTIVE(f(f(mark(y0)))) → c5(F(mark(mark(y0))), ACTIVE(f(mark(y0))))
ACTIVE(f(f(ok(y0)))) → c5(F(mark(ok(y0))), ACTIVE(f(ok(y0))))
ACTIVE(f(f(found(y0)))) → c5(F(mark(found(y0))), ACTIVE(f(found(y0))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(TOP(check(z0)), CHECK(z0))
ACTIVE(f(z0)) → c5(F(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(F(check(z0)), CHECK(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

TOP, CHECK, ACTIVE, F

Compound Symbols:

c8, c9, c7, c10, c5, c7, c10, c2, c5, c3, c4

(55) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 3 leading nodes:

ACTIVE(f(f(found(y0)))) → c5(F(mark(found(y0))), ACTIVE(f(found(y0))))
ACTIVE(f(f(ok(y0)))) → c5(F(mark(ok(y0))), ACTIVE(f(ok(y0))))
ACTIVE(f(f(mark(y0)))) → c5(F(mark(mark(y0))), ACTIVE(f(mark(y0))))

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
ACTIVE(f(f(f(y0)))) → c5(F(mark(f(y0))), ACTIVE(f(f(y0))))
ACTIVE(f(f(f(f(y0))))) → c5(F(mark(f(f(y0)))), ACTIVE(f(f(f(y0)))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

TOP, CHECK, ACTIVE, F

Compound Symbols:

c8, c9, c7, c10, c5, c7, c10, c2, c5, c3, c4

(57) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
TOP(mark(z0)) → c7(CHECK(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
ACTIVE(f(f(f(f(y0))))) → c5(ACTIVE(f(f(f(y0)))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

TOP, CHECK, ACTIVE, F

Compound Symbols:

c8, c9, c7, c10, c5, c7, c10, c2, c5, c3, c4

(59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace TOP(mark(z0)) → c7(CHECK(z0)) by

TOP(mark(f(y0))) → c7(CHECK(f(y0)))
TOP(mark(f(f(f(y0))))) → c7(CHECK(f(f(f(y0)))))
TOP(mark(f(f(y0)))) → c7(CHECK(f(f(y0))))

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
ACTIVE(f(f(f(f(y0))))) → c5(ACTIVE(f(f(f(y0)))))
TOP(mark(f(f(f(y0))))) → c7(CHECK(f(f(f(y0)))))
TOP(mark(f(f(y0)))) → c7(CHECK(f(f(y0))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(active(c)) → c8(TOP(mark(c)))
TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

TOP, CHECK, ACTIVE, F

Compound Symbols:

c8, c9, c10, c5, c7, c7, c10, c2, c5, c3, c4

(61) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

TOP(active(c)) → c8(TOP(mark(c)))

(62) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
ACTIVE(f(f(f(f(y0))))) → c5(ACTIVE(f(f(f(y0)))))
TOP(mark(f(f(f(y0))))) → c7(CHECK(f(f(f(y0)))))
TOP(mark(f(f(y0)))) → c7(CHECK(f(f(y0))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

TOP, CHECK, ACTIVE, F

Compound Symbols:

c9, c10, c5, c7, c7, c10, c2, c5, c3, c4

(63) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) by

TOP(found(f(z0))) → c9(TOP(f(active(z0))), ACTIVE(f(z0)))
TOP(found(f(z0))) → c9(TOP(mark(z0)), ACTIVE(f(z0)))

(64) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
ACTIVE(f(f(f(f(y0))))) → c5(ACTIVE(f(f(f(y0)))))
TOP(mark(f(f(f(y0))))) → c7(CHECK(f(f(f(y0)))))
TOP(mark(f(f(y0)))) → c7(CHECK(f(f(y0))))
TOP(found(f(z0))) → c9(TOP(f(active(z0))), ACTIVE(f(z0)))
TOP(found(f(z0))) → c9(TOP(mark(z0)), ACTIVE(f(z0)))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

TOP(found(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

CHECK, ACTIVE, TOP, F

Compound Symbols:

c10, c5, c7, c7, c10, c2, c5, c3, c4, c9

(65) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

CHECK(f(z0)) → c10(CHECK(z0))
ACTIVE(f(f(f(z0)))) → c5(F(f(f(active(z0)))), ACTIVE(f(f(z0))))
TOP(mark(f(f(z0)))) → c7(TOP(f(f(check(z0)))), CHECK(f(f(z0))))
TOP(mark(f(z0))) → c7(CHECK(f(z0)))
CHECK(f(f(f(z0)))) → c10(F(f(f(check(z0)))), CHECK(f(f(z0))))
CHECK(f(f(z0))) → c10(CHECK(f(z0)))
ACTIVE(f(f(f(z0)))) → c5(ACTIVE(f(f(z0))))
ACTIVE(f(f(f(f(y0))))) → c5(ACTIVE(f(f(f(y0)))))
TOP(mark(f(f(f(y0))))) → c7(CHECK(f(f(f(y0)))))
TOP(mark(f(f(y0)))) → c7(CHECK(f(f(y0))))
TOP(found(f(z0))) → c9(TOP(f(active(z0))), ACTIVE(f(z0)))
TOP(found(f(z0))) → c9(TOP(mark(z0)), ACTIVE(f(z0)))

(66) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))
Tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:

active, f, check

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4

(67) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

active(f(z0)) → f(active(z0))
active(f(z0)) → mark(z0)
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
f(found(z0)) → found(f(z0))
check(f(z0)) → f(check(z0))
check(z0) → start(match(f(X), z0))

(68) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
S tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
K tuples:

F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
Defined Rule Symbols:none

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4

(69) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
We considered the (Usable) Rules:none
And the Tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(found(x1)) = x1   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = [1] + x1   

(70) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
S tuples:none
K tuples:

F(ok(ok(y0))) → c3(F(ok(y0)))
F(ok(found(y0))) → c3(F(found(y0)))
F(ok(mark(mark(y0)))) → c3(F(mark(mark(y0))))
F(ok(mark(ok(y0)))) → c3(F(mark(ok(y0))))
F(ok(mark(found(y0)))) → c3(F(mark(found(y0))))
F(found(found(y0))) → c4(F(found(y0)))
F(found(mark(mark(y0)))) → c4(F(mark(mark(y0))))
F(found(mark(ok(y0)))) → c4(F(mark(ok(y0))))
F(found(mark(found(y0)))) → c4(F(mark(found(y0))))
F(found(ok(ok(y0)))) → c4(F(ok(ok(y0))))
F(found(ok(found(y0)))) → c4(F(ok(found(y0))))
F(found(ok(mark(mark(y0))))) → c4(F(ok(mark(mark(y0)))))
F(found(ok(mark(ok(y0))))) → c4(F(ok(mark(ok(y0)))))
F(found(ok(mark(found(y0))))) → c4(F(ok(mark(found(y0)))))
F(mark(mark(y0))) → c2(F(mark(y0)))
F(mark(ok(y0))) → c2(F(ok(y0)))
F(mark(found(y0))) → c2(F(found(y0)))
Defined Rule Symbols:none

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c4

(71) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(72) BOUNDS(1, 1)